| Definitions | constR{$x:ut2}(T; c; i), inl x , ( x,y L. P(x;y)), A || B, R-loc(R), Rds(R), Rda(R), R-base-domain(R), p = q, R-frame-compat(A;B), R-interface-compat(A;B), Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), Rframe?(x1), Rframe-x(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Reffect-ds(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsframe-tag(x1), Rsends-g(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rrframe?(x1), Rrframe-x(x1), Rpre-ds(x1), Rpre-a(x1), Rrframe-L(x1), Reffect-knd(x1), Reffect-T(x1), Rsends?(x1), Rsends-knd(x1), Rsends-l(x1), Rsends-dt(x1), Rsends-T(x1), "$x", eqof(d), Atom2Deq, eq_atom$n(x;y), (i = j), P    Q,   b, a = b, f || g, IdDeq, x : v, KindDeq,  x:A.B(x), Void,  ,  x.A(x), Top, {i..j }, i  j < k, P & Q, R-discrete_compat(A;B), Reffect-discrete(A), Rinit-discrete(A), Reffect?(x1), Reffect-x(x1), Reffect-f(x1), Rinit?(x1), Rinit-x(x1), Rinit-v(x1), xL. P(x),  b,  x:A. B(x), A c B, ||as||, Dec(P), P  Q, #$n, A B, s ~ t,  ,  , SQType(T), P Q, {T}, [car / cdr], [], tl(l), l[i], i z j, i <z j, hd(l), (x l), Unit,  ,  x. t(x), a:A fp B(a), FinProbSpace, x:A B(x), State(ds), x:A. B(x),  , left + right, IdLnk, x:A  B(x), Knd, type List, Rinit(loc;T;x;v), es realizer ind Rinit compseq tag def, True, Rframe(loc;T;x;L), inr x , R-Feasible(R), es realizer ind Rframe compseq tag def, s = t, A, False, a < b,  , {x:A| B(x)} , Realizer, DeclaredType(ds;x), rec(x.A(x)), Atom$n, Normal(T), Id, t T, Type |